COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.s Introduction
C00009 ENDMK
C⊗;
.s Introduction


	This book covers recursive programming in LISP, computation
with symbolic expressions represented by LISP S-expressions,
representation of S-expressions by list structure in the memory
of a computer, and techniques for mathematically proving that programs meet
their specifications.  We cover the following main topics.

1. Writing recursive programs.  Most students will have already
learned to write sequential programs which change an initial state
of a computation to reach a state satisfying a desired condition.
Recursive programming requires inventing functions that give the
answer in terms of the initial information by building it up from
simpler functions and simpler cases of itself.  Either kind of
program is universal, but in practice the techniques are complementary.
The kind of recursion that makes good programs is %2conditional
expression recursion%1 which differs in important respects
from the recursive definitions
familiar to mathematicians.

2. Computing with symbolic expressions represented by list structure
in the memory of a computer.  The LISP S-expressions form a data domain
with a simple and regular structure, and important computations
with symbolic expressions are readily represented as functions
defined by conditional expression recursion.
The examples are taken from tree search, computing with algebraic
and other expressions involving elementary functions,
pattern matching,
and compiling, interpreting and transforming recursive programs.
Recursive programming is the main technique, but the use of sequential
programs is also discussed.

	The student who has completed a course based on this book
should be able to use LISP proficiently for symbolic computation and
in artificial intelligence applications.

3. Proving programs correct.  A major applied task of computer science
is to develop mathematical theory of computation to the point where
a program is not considered complete until it has been proven to
meet its specification and this proof has been checked by a proof-checker
program.  In particular, a university level course in programming
for computer science students should
teach them to prove correct the programs they write in the course.

	This book includes techniques for proving the extensional
correctness of recursive programs in pure LISP, and most of the
programming exercises are within easy range of these techniques.
Thus recent Stanford
examinations have included programming problems together with a
requirement that the solution be proved to meet certain specifications.
Some techniques are available for non-extensional properties such
as the number of operations executed, and some are available for
sequential programs.

	Recursive programs are represented as functions in a first
order theory and are defined by a %2functional equation%1 which is
essentially a copy of the recursive definition and by a %2minimization
schema%1 which is a sentence schema of first order logic with a
free function parameter.  When the function is total the schema can
be dispensed with.  The extensional properties proved are then just
sentences in first order logic, and its familiar apparatus is
available for proofs.  The technique is much more direct and easier to
to use than the methods available for sequential programs
such as %2inductive assertions%1 and the Hoare axiomatization.

	In fact the proofs are
readily computer-checked by Richard Weyhrauch's first order
proof-checker FOL.  However, FOL has so many conventions and runs
rather slowly, so we didn't feel justified in requiring computer
checking of the proofs in the course on which this book is based.
We may be able to include computer proof-checking in a future version
of the course and a future edition of the book.

	Additional theoretical topics include the universal LISP function,
%2eval%1 which also serves as a LISP interpreter, %2abstract syntax%1
which enables convenient proofs of the correctness of a simple compiler,
and a slight discussion of computability.

	An additional applied topic is syntax directed computation.